Section: New Results

Linear Absolute Value Relation Analysis

Participants : Liqian Chen [National Laboratory for Parallel and Distributed Processing, Changsha, P. R. China] , Antoine Miné, Ji Wang [National Laboratory for Parallel and Distributed Processing, Changsha, P. R. China] , Patrick Cousot.

We present in [15] an abstract domain dealing with linear inequalities involving variables together with their absolute values. It is an extension of the classical linear relation analysis, which permits to deal with some non convex numerical sets. A first nice result states the equivalence between these “linear absolute value inequalities” (AVI) and “interval linear inequalities”, and “extended linear complementary inequalities” (XLCP, pairs of positive solutions whose pairwise components are not both not zero). The key contribution is the extension of the double-description of polyhedra to XLCP solutions, which is then used to define the standard operations on AVI. The method has been implemented, and experiments show interesting results, with reasonable performances with respect to linear relation analysis.